
\addchap{Preface}

\global\long\def\gunderline#1{\mathunderline{greenunder}{#1}}%
\global\long\def\bef{\forwardcompose}%
\global\long\def\bbnum#1{\custombb{#1}}%
This book is at once a reference text and a tutorial that teaches
functional programmers how to reason mathematically about types and
code, in a manner directly relevant to software practice.

The material ranges from introductory to advanced. %
\begin{comment}
Readers will need to learn some difficult concepts through prolonged
mental concentration and effort. 
\end{comment}
The book assumes a certain amount of mathematical experience, at the
level of familiarity with high-school algebra or calculus.

The vision of this book is to explain the mathematical theory that
guides the practice of functional programming. So, all mathematical
developments in this book are motivated by practical programming issues
and are accompanied by Scala code illustrating their usage. For instance,
the laws for standard typeclasses (functors, monads, etc.) are first
motivated heuristically through code examples. Only then the laws
are formulated as mathematical equations and rigorously proved. 

To achieve a clearer presentation of the material, the book uses some
non-standard notations (Appendix~\ref{chap:Appendix-Notations})
and terminology (Appendix~\ref{chap:Appendix-Glossary-of-terms}).
The presentation is self-contained, defining and explaining all required
ideas, notations, and Scala language features. 

Each concept and technique is motivated and explained to make it as
simple as possible%
\begin{comment}
(\textsf{``}but not simpler\textsf{''})
\end{comment}
{} and also clarified via solved examples and exercises, which the readers
will be able to solve after absorbing the preceding material. More
difficult examples and exercises are marked by an asterisk ({*}).

A software engineer needs to know only a few fragments of mathematical
theory; namely, the fragments that answer questions arising in the
practice of functional programming. So, this book keeps theoretical
material at the minimum; \emph{ars longa, vita brevis}. (Chapter~\ref{chap:Applied-functional-type}
discusses the scope of the required theory.) Mathematical generalizations
are not pursued beyond proven practical relevance or immediate pedagogical
usefulness. This reduces the required mathematical knowledge to first
notions of category theory, type theory, and formal logic. Concepts
such as functors or natural transformations arise organically from
the practice of reasoning about code and are introduced without reference
to category theory. This book does not use \textsf{``}introduction/elimination
rules\textsf{''}, \textsf{``}strong normalization\textsf{''}, \textsf{``}complete partial orders\textsf{''},
\textsf{``}adjoint functors\textsf{''}, \textsf{``}pullbacks\textsf{''}, or \textsf{``}topoi\textsf{''}, because learning
these concepts will not help a programmer write code. 

This book is also \emph{not} an introduction to current theoretical
research in functional programming. Instead, the focus is on material
known to be practically useful. That includes constructions such as
the \textsf{``}filterable functor\textsf{''} and \textsf{``}applicative contrafunctor\textsf{''} but
excludes a number of theoretical developments that do not (yet?) appear
to have significant applications.

The first part of the book is for beginners in functional programming.
Readers already familiar with functional programming could skim the
glossary (Appendix~\ref{chap:Appendix-Glossary-of-terms}) to see
the unfamiliar terminology and then start the book with Chapter~\ref{chap:5-Curry-Howard}.

Chapters~\ref{chap:5-Curry-Howard}\textendash \ref{chap:Functors,-contrafunctors,-and}
begin using the code notation, such as Eq.~(\ref{eq:f-functor-exponential-def-of-fmap}).
If that notation still appears hard to follow after going through
Chapters~\ref{chap:5-Curry-Howard}\textendash \ref{chap:Functors,-contrafunctors,-and},
readers could benefit from working through Chapter~\ref{chap:Reasoning-about-code},
which summarizes the code notation more systematically and clarifies
it with additional examples.

All code examples are intended only for explanation and illustration.
As a rule, the code is not optimized for performance or stack safety.

The author thanks Joseph Kim and Jim Kleck for doing some of the exercises
and reporting some errors in earlier versions of this book. The author
also thanks Bill Venners for many helpful comments on the draft, and
Harald Gliebe and Philip Schwarz for contributing corrections to the
text via \texttt{github}. The author is grateful to Frederick Pitts
and several anonymous \texttt{github} contributors who reported errors
in the draft and made helpful suggestions.

\addsec{Formatting conventions used in this book}
\begin{itemize}
\item Text in boldface indicates a new concept or term that is being defined
at that place in the text. Italics means logical emphasis. Example:
\end{itemize}
\begin{quotation}
An \textbf{aggregation\index{aggregation}} is a function from a sequence
of values to a \emph{single} value.
\end{quotation}
\begin{itemize}
\item Equations are numbered per chapter: Eq.~(\ref{eq:prime-formula-function}).
Statements, examples, and exercises are numbered per subsection: Example~\ref{subsec:ch1-aggr-Example-6}
is in subsection~\ref{subsec:Aggregation-solved-examples}, which
belongs to Chapter~\ref{chap:1-Values,-types,-expressions,}.
\item Scala code is written inline using a small monospaced font, such as
\lstinline!flatMap! or \lstinline!val a = "xyz"!. Longer code examples
are written in separate code blocks and may also show the Scala interpreter\textsf{'}s
output for certain lines:
\begin{lstlisting}[mathescape=true]
val s = (1 to 10).toList

scala> s.product
res0: Int = 3628800 
\end{lstlisting}
\item In the introductory chapters, type expressions and code examples are
written in the syntax of Scala. Starting from Chapters~\ref{chap:Higher-order-functions}\textendash \ref{chap:5-Curry-Howard},
the book introduces a new notation for types where, e.g., the Scala
type expression \lstinline!((A, B)) => Option[A]! is written as $A\times B\rightarrow\bbnum 1+A$.
Also, a new notation for code is introduced and developed in Chapters~\ref{chap:5-Curry-Howard}\textendash \ref{chap:Reasoning-about-code}
for efficient reasoning about typeclass laws. For example, the functor
composition law is written in the code notation as
\[
f^{\uparrow L}\bef g^{\uparrow L}=\left(f\bef g\right)^{\uparrow L}\quad,
\]
where $L$ is a functor and $f^{:A\rightarrow B}$ and $g^{:B\rightarrow C}$
are arbitrary functions of the specified types. The notation $f^{\uparrow L}$
denotes the function $f$ lifted to the functor $L$ and replaces
Scala\textsf{'}s syntax \lstinline!x.map(f)! where \lstinline!x! is of type
\lstinline!L[A]!. The symbol $\bef$ denotes the forward composition
of functions (Scala\textsf{'}s \lstinline!andThen! method). Appendix~\ref{chap:Appendix-Notations}
summarizes the notation conventions for types and code.
\item Frequently used methods of standard typeclasses, such as \lstinline!pure!,
\lstinline!flatMap!, \lstinline!flatten!, \lstinline!filter!, etc.,
are denoted by shorter words and are labeled by the type constructor
they belong to. For instance, the text talks about typeclass methods
\lstinline!pure!, \lstinline!flatten!, and \lstinline!flatMap!
for a monad $M$ but denotes the same methods by $\text{pu}_{M}$,
$\text{ftn}_{M}$, and $\text{flm}_{M}$ when writing code formulas.
\item Derivations are written in a two-column format where the right column
contains formulas in the code notation and the left column gives a
line-by-line explanation or indicates the property or law used to
derive the expression at right. A green underline in an expression
shows the parts to be rewritten using the law or equation indicated
in the \emph{next} line:
\begin{align*}
{\color{greenunder}\text{expect to equal }\text{pu}_{M}:}\quad & \gunderline{\text{pu}_{M}^{\uparrow\text{Id}}}\bef\text{pu}_{M}\bef\text{ftn}_{M}\\
{\color{greenunder}\text{lifting to the identity functor}:}\quad & =\text{pu}_{M}\bef\gunderline{\text{pu}_{M}\bef\text{ftn}_{M}}\\
{\color{greenunder}\text{left identity law of }M:}\quad & =\text{pu}_{M}\quad.
\end{align*}
A green underline is sometimes also used at the last step of a derivation,
to indicate the sub-expression that resulted from the most recent
rewriting. Other than providing hints to help  remember the steps
of a derivation, the green underlines \emph{play no role} in symbolic
calculations.
\item The symbol $\square$ is used occasionally to indicate the end of
a derivation or a proof.
\end{itemize}

